Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0

The replacement map contains the following entries:

f: {1}
0: empty set
cons: {1}
s: {1}
p: {1}


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0

The replacement map contains the following entries:

f: {1}
0: empty set
cons: {1}
s: {1}
p: {1}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0

The replacement map contains the following entries:

f: {1}
0: empty set
cons: {1}
s: {1}
p: {1}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {f, s, p, F, P} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

F(s(0)) → F(p(s(0)))
F(s(0)) → P(s(0))


The hidden terms of R are:

f(s(0))

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

U(f(s(0))) → F(s(0))

The TRS R consists of the following rules:

f(0) → cons(0, f(s(0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0

The set Q consists of the following terms:

f(0)
f(s(0))
p(s(0))


The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.
The rules F(s(0)) → F(p(s(0))) and F(s(0)) → F(p(s(0))) form no chain, because ECapµR'(F(s(0))) = F(s(x_1)) does not unify with F(p(s(0))).
R' =

( 0, p(s(0)))


The rules F(s(0)) → F(p(s(0))) and F(s(0)) → P(s(0)) form no chain, because ECapµR'(F(s(0))) = F(s(x_1)) does not unify with F(p(s(0))).
R' =

( 0, p(s(0)))